…e dimension formula

Adds `CuspFormSubmodule.lean` providing the cusp form submodule of modular
forms together with API, and `DimensionFormulas/LevelOne.lean` proving the
classical dimension formula for spaces of level one modular forms.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Targeted fixes from PR leanprover-community#37789 review:
- `cuspFormSubmodule` and `equivCuspFormSubmodule`: make `Γ`/`k` explicit
- `isCuspForm_iff`: shorter proof
- `ofMulDiscriminant`: simplify cusp-form coeff zero argument
- `divDiscriminant.holo'`: golf by inlining the differentiability subgoals
- `rank_eq_one_add_rank_cuspForm`: take `hk : 3 ≤ k` over `ℕ`
- `discriminant_eq_E4_cube_sub_E6_sq`: restate as `Δ = (E₄³ - E₆²)/1728`,
  drop inline proof comments, fold redundant `have`s
- `exists_smul_eq_of_rank_one`: use `finrank_eq_one_iff_of_nonzero'` from mathlib
- Move `one_mem_strictPeriods_SL` to `LevelOne.lean` so the haveI workaround
  in `EisensteinSeries.E_qExpansion_coeff` can be dropped

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…ula proofs

- `discriminant_eq_E4_cube_sub_E6_sq`: hoist `hmcast` (used 3x) above its
  use, drop redundant calc step `_ = (CuspForm.toModularFormₗ g) z := rfl`
- `weight_two_eq_zero_of_not_cuspForm`: drop `hc0`, fold the c4/c6
  substitutions directly into `heq4`/`heq6` rather than via separate
  `hc4_eq`/`hc6_eq` + `rw`, replace the by_contra finale with
  `pow_eq_zero_iff`/`mul_eq_zero`

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Add public `noncomputable abbrev`s `ModularForm.E₄ : ModularForm 𝒮ℒ 4` and
`ModularForm.E₆ : ModularForm 𝒮ℒ 6` for the normalised level 1 Eisenstein
series of weights 4 and 6. Use them throughout `DimensionFormulas/LevelOne.lean`
to drop the awkward `E (show 3 ≤ 4 by norm_num)` and `set E4 := …` patterns.

The `abbrev` (rather than `def` or notation) is required so all uses share
a single underlying proof of `3 ≤ 4` / `3 ≤ 6`, which lets simp lemmas about
their q-expansions match consistently.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…oor_sub_div`

Adds the lemma `⌊k / a⌋₊ = 1 + ⌊(k - a) / a⌋₊` for `0 < a ≤ k` over a linear
ordered field, generalising the local `floor_lem1` helper that was buried in
`DimensionFormulas/LevelOne.lean`. Inline the helper at its single use site
in `dimension_level_one`.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…lpers up to DedekindEta

Adds three q-coordinate lemmas to `DedekindEta.lean`:
- `multipliable_one_sub_pow {q : ℂ} (hq : ‖q‖ < 1)`: pointwise multipliability
- `multipliableLocallyUniformlyOn_one_sub_pow`: local uniform convergence on the
  open unit disc
- `differentiableOn_tprod_one_sub_pow_pow (k : ℕ)`: differentiability of the
  k-th power of the product on the open unit disc

These cover the case `q = 0` (the cusp at infinity), which the existing eta-side
lemmas (`multipliableLocallyUniformlyOn_eta` etc., stated on `ℍₒ`) cannot.

In `Discriminant.lean`, deletes the three private helpers
`multipliable_one_sub_pow`, `tendstoLocallyUniformlyOn_eta_prod`,
`differentiableWithinAt_eta_prod_pow`, and rewrites `discriminant_cuspFunction_eqOn`
and `discriminant_qExpansion_coeff_one` to work on the full open unit disc
`Metric.ball 0 1` (instead of the arbitrary `Metric.ball 0 (1/2)`) and to call
the new helpers from `DedekindEta.lean`.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…-coord base

Rather than having parallel q-coord and z-coord proofs of the same convergence
facts about the eta product, derive the z-coord versions from the q-coord ones
by composing with `Periodic.qParam 1 : ℍₒ → Metric.ball 0 1`.

- `multipliableLocallyUniformlyOn_eta` is now derived from
  `multipliableLocallyUniformlyOn_one_sub_pow` via `TendstoLocallyUniformlyOn.comp`,
  shrinking the proof from ~14 lines to ~7.
- `differentiableAt_eta_tprod` now derives from `differentiableOn_tprod_one_sub_pow`
  by chain rule (instead of going through the eta-side multipliable lemma).
- `summable_eta_q` switched to `norm_qParam_lt_one` (which the q-coord material
  already uses) for consistency.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…lyOn_eta`

`hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` is `Iff.rfl`, so the
two `rw` calls in the previous proof are unnecessary — a type ascription on the
underlying `HasProdLocallyUniformlyOn` is enough to invoke
`TendstoLocallyUniformlyOn.comp` via dot notation. Collapse the proof to a
6-line term-mode expression.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Extracts helper lemmas to shorten the two main proofs:

- `tendsto_valueAtInfty`: a modular form whose `valueAtInfty` is `c` tends to
  `c` along `atImInfty`. Used in `E4_cube_sub_E6_sq_form_isCuspForm`.

- `E4_cube_sub_E6_sq_form` (def): the explicit `ModularForm 𝒮ℒ 12` whose
  pointwise value is `E₄³ - E₆²`, with companion lemmas `_apply`,
  `_isCuspForm`, `_qExpansion_coeff_one`. The main theorem
  `discriminant_eq_E4_cube_sub_E6_sq` is now ~15 lines instead of ~70.

- `coeffZero_eq_zero_of_pow_eq_smul`: the algebraic core of the weight-2
  vanishing argument as a pure power-series fact (no modular forms).
  `weight_two_eq_zero_of_not_cuspForm` becomes a thin wrapper that
  transports the modular-form identities into the power-series form,
  shrinking from ~50 lines to ~25.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…ter decomposition

- `discriminant_eq_E4_cube_sub_E6_sq`: move `hgΔ` back inside the local
  `hc_eq` block (it's only used there), inline `hgF`, and use `simpa` for
  the final step.
- `E4_cube_sub_E6_sq_form_qExpansion_coeff_one`: minor simplification
  collapsing the chained `mcast`/`hmcast` rewrites.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Wraps several lines in the dimension-formula proofs to fit within mathlib's
100-character line length limit. No semantic changes.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…sion lemmas

`E₄` and `E₆` are `noncomputable abbrev`s, so they reduce automatically and the
explicit `show E₄ = E (...) from rfl` step in `E₄_qExpansion_coeff_one` and
`E₆_qExpansion_coeff_one` was unnecessary.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…fomula_lvl1

Adds `CuspForm.toModularForm` and a `Coe (CuspForm Γ k) (ModularForm Γ k)` instance so
cusp forms can be viewed as modular forms automatically. Refactors
`CuspForm.toModularFormₗ` to delegate to this plain function and updates call sites.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…ubmodule

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

…fomula_lvl1

…fomula_lvl1

Restores ModularForm.discriminant_eq_E4_cube_sub_E6_sq, ported from earlier work
(commit 8d90310) and updated to current master's API:
- discriminantCuspForm → CuspForm.discriminant
- cuspForm_twelve_smul_discriminant → CuspForm.exists_smul_discriminant_of_weight_eq_twelve
- qExpansion_sub/qExpansion_smul → ModularFormClass.qExpansion_sub/qExpansion_smul
- The `IsCuspForm` proof uses an algebraic q-expansion split rather than the
  no-longer-available tendsto_valueAtInfty.

Adds supporting lemmas in Discriminant.lean:
- discriminant_cuspFunction_eqOn (private)
- differentiableWithinAt_eta_prod_pow (private; shorter than original since
  differentiableOn_tprod_one_sub_pow_pow is now in mathlib)
- discriminant_qExpansion_coeff_one

Also drops merge-induced duplicates of master lemmas (summable_eta_q,
multipliableLocallyUniformlyOn_eta, differentiableOn_tprod_one_sub_pow,
differentiableOn_tprod_one_sub_pow_pow, one_mem_strictPeriods_SL) and removes
two unused/duplicating helpers (floor_div_eq_one_add_floor_sub_div, which is
too specific for a top-level file and unused, and ModularForm.ofSubgroupEq,
which duplicates mcast).

Applies findings from /simplify code review:

- Extract the duplicated `qExpansion_sub` rewrite chain into a shared
  `E₄CubeSubE₆SqForm_qExpansion_eq` helper. Both `_isCuspForm` and
  `_qExpansion_coeff_one` now reduce to a one-line `rw` of this helper
  (~16 lines saved).
- `linear_combination (1 / 1728 : ℂ) * h1728` → `linear_combination h1728 / 1728`.
- Rename `E4_cube_sub_E6_sq_form` → `E₄CubeSubE₆SqForm` (camelCase + subscripts
  per mathlib def naming convention) and `discriminant_eq_E4_cube_sub_E6_sq`
  → `discriminant_eq_E₄_cube_sub_E₆_sq`.
- Use `ball 0 1` instead of `ball 0 (1/2)` in `discriminant_cuspFunction_eqOn`
  and `discriminant_qExpansion_coeff_one` (the actual constraint is `‖q‖ < 1`),
  which lets `differentiableOn_tprod_one_sub_pow_pow` apply directly and
  removes the now-unnecessary `differentiableWithinAt_eta_prod_pow` helper.

Drops `(... : ℍ → ℂ)` type ascriptions where the surrounding term already
forces the coercion (`qExpansion 1 E₄`, `cuspFunction 1 Δ`,
`qExpansion 1 E₄CubeSubE₆SqForm`, etc.). Also reflows the affected
declarations to fit the 100-character line limit.

…²) / 1728

Adds `ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded`, the analogue of
`discriminant_eq_E₄_cube_sub_E₆_sq` in the graded ring `⨁ k, ModularForm 𝒮ℒ k`:

  DirectSum.of (ModularForm 𝒮ℒ) 12 (CuspForm.discriminant : ModularForm 𝒮ℒ 12) =
    (1 / 1728 : ℂ) • (DirectSum.of (ModularForm 𝒮ℒ) 4 E₄ ^ 3 -
      DirectSum.of (ModularForm 𝒮ℒ) 6 E₆ ^ 2)

The proof reduces to the pointwise identity via `DirectSum.of_mul_of`, `congr 1`,
and `ext`, then closes by `discriminant_eq_E₄_cube_sub_E₆_sq` and `ring`.

In `discriminant_eq_E₄_cube_sub_E₆_sq_graded`, replace `(by norm_num)` proofs
of `4 + 4 + 4 = 12` and `6 + 6 = 12` with `(by decide)` (kernel reduction).

Adds `@[simp]` lemmas `ModularForm.mcast_apply` and `CuspForm.mcast_apply`
saying `mcast h f hΓ z = f z` (true by `rfl`). These let `simp` automatically
unfold `mcast` in pointwise reasoning, and are useful API for any future
proofs that mix `ModularForm.mcast`/`CuspForm.mcast` with `simp`-based
function-level rewriting.

The simp lemmas were unused — `change` in `discriminant_eq_E₄_cube_sub_E₆_sq_graded`
goes through defeq directly, and the `simp only`-based alternatives I tried
didn't close the goal. Removing per "no unused API" guideline; can be re-added
later when there's a proof that benefits.

This reverts commit 8de2aff.

Extract two helpers from the proof:
* `reduced_isWeightedHomogeneous_eq_monomial`: a reduced (`d 0 < 3` for all
  support `d`) weighted-homogeneous polynomial of weight `n` equals the monomial
  at any of its support points.
* `evalE₄E₆_monomial_qExpansion_coeff_zero`: the q-expansion-coeff-0 of
  `evalE₄E₆ (monomial d c)` evaluated at the matching weight equals `c`.

`reduced_part_eq_zero` is now 36 lines instead of 62.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…p` and `surj_of_weight`

* Extract `support_sum_lt_after_sub_δ_piece` from `whomog_poly_Delta_decomp`
  (the support-sum-decreases sub-proof, ~16 lines).
* Extract `evalE₄E₆_X_sq` and `evalE₄E₆_X0_X1` simp-style API lemmas, used
  in the weight-8 and weight-10 base cases of `surj_of_weight`.

`whomog_poly_Delta_decomp`: 67 → 52 lines.
`surj_of_weight`: 51 → 45 lines.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…-length fixes

* Rename `whomog_*` → `weightedHomogeneous_*`
* Rename `mvpoly_*` → `mvPolynomial_*`
* Rename `eval_discriminantPoly_mul_zero_imp` → `eval_discriminantPoly_mul_eq_zero_imp_eval_eq_zero`
* Rename `unique_small_weight_soln` → `unique_small_weight_solution`
* Rename `no_wt_monomial_*` → `no_weight_monomial_*`
* Remove the `Δ = (E₄³ - E₆²) / 1728` section header
* Reformat a few long signatures.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Reformat declaration signatures and proof terms that exceeded the 100-char
linter limit; reformat the `surj_of_weight` weight-{4,6,8,10} branches and
the `E₄E₆_generate` proof header.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…surj_of_weight`

Replace `interval_cases n` (12 sub-goals, half of which only dismiss odd n) with
a single `obtain rfl | rfl | rfl | rfl | rfl | rfl : n = 0 ∨ ... ∨ n = 10` so
the proof has 6 branches instead of 12.

`surj_of_weight`: 51 → 47 lines.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…uspForm_eq_discriminant_mul`

* Reformat `mul_ne_zero`, `directSumOf_cast_eq`, `cast_modularForm_apply`,
  `discriminant_mem_range_evalE₄E₆`, `directSumOf_evalE₄E₆_monomial_apply`,
  and `evalE₄E₆_whc_grade` to fit within 100 chars.
* Use `refine ... <| ... ?_` to merge the four `apply`/`refine` lines at the
  top of `cuspForm_eq_discriminant_mul` (28 → 24 lines).

Down to 3 lines (all 103–105 chars) over the linter limit.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…Fin 2 → ℕ)`

Drop the standalone `E₄E₆Weight` definition (a junk one-liner with no API)
and inline it at each use site as `(![4, 6] : Fin 2 → ℕ)`.

The type ascription is necessary: without it, `![4, 6]` elaborates to different
`M`'s in `Finsupp.weight (w : σ → M)` depending on the surrounding context
(`Fin 2 → ℕ` vs `Fin 2 → ℤ`), which breaks rewrites between sibling lemmas.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…nd tactic split

* Split the surviving `;`-chained tactic in `cuspForm_eq_discriminant_mul`
  (`change ...; ring` → two-line bullet).
* Reformat declaration signatures and proof bodies that exceeded the 100-char
  linter limit (mostly induced by the inlined `(![4, 6] : Fin 2 → ℕ)`).

No remaining lines exceed 100 chars.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Make several helpers ready to be lifted to mathlib core in a separate PR:

* `mul_ne_zero` → `modularForm_mul_ne_zero`: generalize from `𝒮ℒ` to any
  `Γ` with `[HasDetPlusMinusOne]` and any `(hh : 0 < h)` (`hΓ : h ∈ Γ.strictPeriods`).
* `directSumOf_cast_eq` → `directSum_of_eq_cast`: generalize from `ModularForm 𝒮ℒ`
  to any indexed family `β : ι → Type*` of `AddCommMonoid`s.
* `cast_modularForm_apply` → `modularForm_cast_apply`: generalize from `𝒮ℒ` to
  any `Γ`.
* `weightedHomogeneous_eq_zero_of_no_monomials`,
  `weightedHomogeneous_unique_monomial`: generalize from `(![4, 6] : Fin 2 → ℕ)`
  to any weight function `w : σ → M` and any `CommSemiring R`.

Plus another `surj_of_weight` golf: weight-0 case 4 → 3 lines.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* `monomial_fin2_eq`: generalize from `ℂ` to any `CommSemiring R`.
* Extract `weight_fin2 : Finsupp.weight w d = d 0 * w 0 + d 1 * w 1` (general
  Fin-2 weight identity) and let `weight_eq_4a_6b` be a one-line specialization.

These continue to prepare helpers for migration to mathlib core in the
forthcoming Group-A / Group-B PR splits.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…s, proof tightening

Naming (no abbreviations):
- evalE₄E₆_whc_grade → evalE₄E₆_apply_eq_zero_of_ne
- evalE₄E₆_whc_eq_single → evalE₄E₆_eq_of_apply
- evalE₄E₆_mono_grade → evalE₄E₆_X_pow_mul_apply_eq_zero_of_ne
- evalE₄E₆_monomial_grade → evalE₄E₆_monomial_apply_eq_zero_of_ne
- directSumOf_evalE₄E₆_monomial_apply → directSum_of_E₄_pow_mul_E₆_pow_apply

New general helpers (candidates for upstream PRs):
- weightedHomogeneous_sub: sub of weighted-homogeneous polys
- directSum_of_eq_sub_add_smul: of i f = of i (f - c•g) + c • of i g

Proof simplifications:
- monomial_qExpansion_coeff_zero_eq_one: factor through qExpansionRingHom_apply directly
- discriminantPoly_isWeightedHomogeneous: use weightedHomogeneous_sub
- evalE₄E₆_apply_eq_zero_of_ne / evalE₄E₆_component_eq: DirectSum.sum_apply, DirectSum.add_apply
- discriminantPoly_piece_eq_monomial_sub: clean up inline show chains
- per_weight_injective_zero: use weightedHomogeneous_unique_monomial
- reduced_part_eq_zero: collapse two-step Q.map_add → coeff into one rewrite
- surj_at_weight_inductive: use directSum_of_eq_sub_add_smul helper

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…y#38806

- Discriminant.lean: convert single `simp` for `discriminant_qExpansion_coeff_one`
  to a 3-step `calc` proof for robustness.
- Basic.lean: add `ModularForm.pow` (with `coe_pow` simp lemma).
- QExpansion.lean: add `ModularForm.qExpansion_pow`.
- GradedRing.lean: use `pow` and `qExpansion_pow` in the `E₄³ - E₆²` def.
- QExpansion.lean: move `cuspFunction_smul/neg/add/sub` and
  `qExpansion_smul/neg/add/sub` from `ModularFormClass` to `ModularForm`
  namespace, per the convention that lemmas about `Foo` go in the `Foo`
  namespace even when their input is class-generic.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…dedRing

This was missed by the cherry-pick because the graded-ring branch has an
extra usage in `sub_smul_qExpansion_coeff_zero_isCuspForm` that wasn't on
the discriminant branch.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…aded ring

Adds five lemmas extracted from the upcoming graded-ring PR (leanprover-community#38813), so that
that PR can be reviewed in smaller pieces:

* `DirectSum.of_eq_of_eq` (Algebra/DirectSum/Basic): cast indices in `of`.
* `DirectSum.of_eq_sub_add_smul` (Algebra/DirectSum/Module): the identity
  `of i f = of i (f - c•g) + c • of i g`.
* `ModularForm.cast_apply` (NumberTheory/ModularForms/Basic): a ModularForm
  cast through a weight equality has the same pointwise values.
* `ModularForm.mul_ne_zero` (NumberTheory/ModularForms/QExpansion): the
  product of two non-zero modular forms is non-zero (via integral domain
  structure of `PowerSeries ℂ`).
* `ModularForm.sub_smul_isCuspForm` (NumberTheory/ModularForms/CuspFormSubmodule):
  for level-1 forms `f, g` with `(qExpansion 1 g).coeff 0 = 1`, the form
  `f - (qExpansion 1 f).coeff 0 • g` is a cusp form.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…f_no_monomials, eq_monomial_of_unique_weight

Adds three weighted-homogeneous API lemmas extracted from the upcoming
graded-ring PR (leanprover-community#38813):

* `IsWeightedHomogeneous.sub`: difference of weighted-homogeneous polynomials
  of degree `n` is weighted-homogeneous of degree `n` (mirrors `add`,
  requires `CommRing R`).
* `IsWeightedHomogeneous.eq_zero_of_no_monomials`: a weighted-homogeneous
  polynomial of degree `n` is zero if no monomial has weight `n`.
* `IsWeightedHomogeneous.eq_monomial_of_unique_weight`: a weighted-homogeneous
  polynomial of degree `n` whose support is concentrated at a single `d₀`
  equals `monomial d₀ (coeff d₀ φ)`.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Removes ~70 lines of local API helpers from GradedRing.lean now that they
are added to the appropriate mathlib files via the two prerequisite PRs:

* From `Mathlib/NumberTheory/ModularForms/Basic.lean`: `ModularForm.cast_apply`.
* From `Mathlib/Algebra/DirectSum/Basic.lean`: `DirectSum.of_eq_of_eq`.
* From `Mathlib/Algebra/DirectSum/Module.lean`: `DirectSum.of_eq_sub_add_smul`.
* From `Mathlib/NumberTheory/ModularForms/QExpansion.lean`: `ModularForm.mul_ne_zero`.
* From `Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean`:
  `ModularForm.sub_smul_isCuspForm`.
* From `Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean`:
  `IsWeightedHomogeneous.sub`, `eq_zero_of_no_monomials`,
  `eq_monomial_of_unique_weight`.

Also fixes the proof of `DirectSum.of_eq_sub_add_smul` to avoid an instance
ambiguity between `AddCommMonoid` and `AddCommGroup` from the section
variables; the proof now uses an explicit `M` declaration.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…aded-ring